STRATEGY =
(LAMBDA (X) (SUPPORT X)) 
SUPPORT-SET-IS: 
¬R(D(THM32,O),THM32) 
UNIT-PREFERENCE =NIL
MERGE =NIL
ORDER =NIL
ANCESTRY =T
DEPTH-BOUND =3
LENGTH-BOUND =2

PARMODULATE =NIL
ELAPSED-TIME =47833

NIL 1 4
1 ¬LE(O,O) 3 4
3 ¬LE(O,D(THM32,D(THM32,O))) ¬LE(O,O) 5 6
4 LE(O,Z447) AXIOM 5
5 ¬LE(O,D(THM32,D(THM32,O))) ¬LE(D(THM32,O),D(THM32,O)) 7 8
6 LE(D(Z459,Z458),D(Z459,Z457)) ¬LE(Z457,Z458) AXIOM 10
7 ¬LE(O,D(THM32,D(THM32,O))) ¬LE(D(THM32,D(THM32,O)),O) 9 15
8 LE(D(Z454,Z456),Z455) ¬LE(D(Z454,Z455),Z456) AXIOM 9
9 ¬R(D(THM32,D(THM32,O)),O) 11 12
11 ¬LE(THM32,D(THM32,O)) 13 14
12 LE(Z440,Z441) ¬R(D(Z440,Z441),O) AXIOM 2
13 ¬LE(THM32,D(THM32,O)) ¬LE(D(THM32,O),THM32) 15 16
14 LE(D(Z442,Z443),Z442) AXIOM 3
15 R(Z449,Z450) ¬LE(Z450,Z449) ¬LE(Z449,Z450) AXIOM 7
16 ¬R(D(THM32,O),THM32) AXIOM -13